u, v:. (u = v)  ((u  v)) 

latex

Up	bool 1, bool 1
Definitions	, t  T, P  Q, x:A. B(x), True, tt, ff, if b then t else f fi , b, p q, p  q, b, Unit, , A, False,
Lemmas	bool wf, btrue neq bfalse